Termination w.r.t. Q of the following Term Rewriting System could not be shown:

Q restricted rewrite system:
The TRS R consists of the following rules:

2(7(x1)) → 1(8(x1))
2(8(1(x1))) → 8(x1)
2(8(x1)) → 4(x1)
5(9(x1)) → 0(x1)
4(x1) → 5(2(3(x1)))
5(3(x1)) → 6(0(x1))
2(8(x1)) → 7(x1)
4(7(x1)) → 1(3(x1))
5(2(6(x1))) → 6(2(4(x1)))
9(7(x1)) → 7(5(x1))
7(2(x1)) → 4(x1)
7(0(x1)) → 9(3(x1))
6(9(x1)) → 9(x1)
9(5(9(x1))) → 5(7(x1))
4(x1) → 9(6(6(x1)))
9(x1) → 6(7(x1))
6(2(x1)) → 7(7(x1))
2(4(x1)) → 0(7(x1))
6(6(x1)) → 3(x1)
0(3(x1)) → 5(3(x1))

Q is empty.


↳ QTRS
  ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

2(7(x1)) → 1(8(x1))
2(8(1(x1))) → 8(x1)
2(8(x1)) → 4(x1)
5(9(x1)) → 0(x1)
4(x1) → 5(2(3(x1)))
5(3(x1)) → 6(0(x1))
2(8(x1)) → 7(x1)
4(7(x1)) → 1(3(x1))
5(2(6(x1))) → 6(2(4(x1)))
9(7(x1)) → 7(5(x1))
7(2(x1)) → 4(x1)
7(0(x1)) → 9(3(x1))
6(9(x1)) → 9(x1)
9(5(9(x1))) → 5(7(x1))
4(x1) → 9(6(6(x1)))
9(x1) → 6(7(x1))
6(2(x1)) → 7(7(x1))
2(4(x1)) → 0(7(x1))
6(6(x1)) → 3(x1)
0(3(x1)) → 5(3(x1))

Q is empty.

Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

21(4(x1)) → 01(7(x1))
51(2(6(x1))) → 41(x1)
91(7(x1)) → 51(x1)
91(x1) → 61(7(x1))
41(x1) → 61(6(x1))
41(x1) → 21(3(x1))
91(7(x1)) → 71(5(x1))
51(9(x1)) → 01(x1)
21(8(x1)) → 41(x1)
51(3(x1)) → 61(0(x1))
41(x1) → 51(2(3(x1)))
71(2(x1)) → 41(x1)
21(4(x1)) → 71(x1)
91(5(9(x1))) → 71(x1)
91(x1) → 71(x1)
41(x1) → 91(6(6(x1)))
01(3(x1)) → 51(3(x1))
41(x1) → 61(x1)
51(2(6(x1))) → 61(2(4(x1)))
91(5(9(x1))) → 51(7(x1))
71(0(x1)) → 91(3(x1))
61(2(x1)) → 71(7(x1))
51(2(6(x1))) → 21(4(x1))
51(3(x1)) → 01(x1)
61(2(x1)) → 71(x1)
21(8(x1)) → 71(x1)

The TRS R consists of the following rules:

2(7(x1)) → 1(8(x1))
2(8(1(x1))) → 8(x1)
2(8(x1)) → 4(x1)
5(9(x1)) → 0(x1)
4(x1) → 5(2(3(x1)))
5(3(x1)) → 6(0(x1))
2(8(x1)) → 7(x1)
4(7(x1)) → 1(3(x1))
5(2(6(x1))) → 6(2(4(x1)))
9(7(x1)) → 7(5(x1))
7(2(x1)) → 4(x1)
7(0(x1)) → 9(3(x1))
6(9(x1)) → 9(x1)
9(5(9(x1))) → 5(7(x1))
4(x1) → 9(6(6(x1)))
9(x1) → 6(7(x1))
6(2(x1)) → 7(7(x1))
2(4(x1)) → 0(7(x1))
6(6(x1)) → 3(x1)
0(3(x1)) → 5(3(x1))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

21(4(x1)) → 01(7(x1))
51(2(6(x1))) → 41(x1)
91(7(x1)) → 51(x1)
91(x1) → 61(7(x1))
41(x1) → 61(6(x1))
41(x1) → 21(3(x1))
91(7(x1)) → 71(5(x1))
51(9(x1)) → 01(x1)
21(8(x1)) → 41(x1)
51(3(x1)) → 61(0(x1))
41(x1) → 51(2(3(x1)))
71(2(x1)) → 41(x1)
21(4(x1)) → 71(x1)
91(5(9(x1))) → 71(x1)
91(x1) → 71(x1)
41(x1) → 91(6(6(x1)))
01(3(x1)) → 51(3(x1))
41(x1) → 61(x1)
51(2(6(x1))) → 61(2(4(x1)))
91(5(9(x1))) → 51(7(x1))
71(0(x1)) → 91(3(x1))
61(2(x1)) → 71(7(x1))
51(2(6(x1))) → 21(4(x1))
51(3(x1)) → 01(x1)
61(2(x1)) → 71(x1)
21(8(x1)) → 71(x1)

The TRS R consists of the following rules:

2(7(x1)) → 1(8(x1))
2(8(1(x1))) → 8(x1)
2(8(x1)) → 4(x1)
5(9(x1)) → 0(x1)
4(x1) → 5(2(3(x1)))
5(3(x1)) → 6(0(x1))
2(8(x1)) → 7(x1)
4(7(x1)) → 1(3(x1))
5(2(6(x1))) → 6(2(4(x1)))
9(7(x1)) → 7(5(x1))
7(2(x1)) → 4(x1)
7(0(x1)) → 9(3(x1))
6(9(x1)) → 9(x1)
9(5(9(x1))) → 5(7(x1))
4(x1) → 9(6(6(x1)))
9(x1) → 6(7(x1))
6(2(x1)) → 7(7(x1))
2(4(x1)) → 0(7(x1))
6(6(x1)) → 3(x1)
0(3(x1)) → 5(3(x1))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 2 SCCs with 8 less nodes.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
            ↳ QDPOrderProof
          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

01(3(x1)) → 51(3(x1))
51(3(x1)) → 01(x1)

The TRS R consists of the following rules:

2(7(x1)) → 1(8(x1))
2(8(1(x1))) → 8(x1)
2(8(x1)) → 4(x1)
5(9(x1)) → 0(x1)
4(x1) → 5(2(3(x1)))
5(3(x1)) → 6(0(x1))
2(8(x1)) → 7(x1)
4(7(x1)) → 1(3(x1))
5(2(6(x1))) → 6(2(4(x1)))
9(7(x1)) → 7(5(x1))
7(2(x1)) → 4(x1)
7(0(x1)) → 9(3(x1))
6(9(x1)) → 9(x1)
9(5(9(x1))) → 5(7(x1))
4(x1) → 9(6(6(x1)))
9(x1) → 6(7(x1))
6(2(x1)) → 7(7(x1))
2(4(x1)) → 0(7(x1))
6(6(x1)) → 3(x1)
0(3(x1)) → 5(3(x1))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].


The following pairs can be oriented strictly and are deleted.


01(3(x1)) → 51(3(x1))
51(3(x1)) → 01(x1)
The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [25,35]:

POL(01(x1)) = 2 + (11/4)x_1   
POL(3(x1)) = 9/4 + (15/4)x_1   
POL(51(x1)) = 9/4 + (2)x_1   
The value of delta used in the strict ordering is 23/16.
The following usable rules [17] were oriented: none



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
            ↳ QDPOrderProof
              ↳ QDP
                ↳ PisEmptyProof
          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

2(7(x1)) → 1(8(x1))
2(8(1(x1))) → 8(x1)
2(8(x1)) → 4(x1)
5(9(x1)) → 0(x1)
4(x1) → 5(2(3(x1)))
5(3(x1)) → 6(0(x1))
2(8(x1)) → 7(x1)
4(7(x1)) → 1(3(x1))
5(2(6(x1))) → 6(2(4(x1)))
9(7(x1)) → 7(5(x1))
7(2(x1)) → 4(x1)
7(0(x1)) → 9(3(x1))
6(9(x1)) → 9(x1)
9(5(9(x1))) → 5(7(x1))
4(x1) → 9(6(6(x1)))
9(x1) → 6(7(x1))
6(2(x1)) → 7(7(x1))
2(4(x1)) → 0(7(x1))
6(6(x1)) → 3(x1)
0(3(x1)) → 5(3(x1))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
            ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

21(4(x1)) → 71(x1)
91(5(9(x1))) → 71(x1)
91(x1) → 71(x1)
51(2(6(x1))) → 41(x1)
41(x1) → 91(6(6(x1)))
91(7(x1)) → 51(x1)
41(x1) → 61(x1)
51(2(6(x1))) → 61(2(4(x1)))
91(7(x1)) → 71(5(x1))
71(0(x1)) → 91(3(x1))
61(2(x1)) → 71(7(x1))
21(8(x1)) → 41(x1)
51(2(6(x1))) → 21(4(x1))
61(2(x1)) → 71(x1)
71(2(x1)) → 41(x1)
21(8(x1)) → 71(x1)

The TRS R consists of the following rules:

2(7(x1)) → 1(8(x1))
2(8(1(x1))) → 8(x1)
2(8(x1)) → 4(x1)
5(9(x1)) → 0(x1)
4(x1) → 5(2(3(x1)))
5(3(x1)) → 6(0(x1))
2(8(x1)) → 7(x1)
4(7(x1)) → 1(3(x1))
5(2(6(x1))) → 6(2(4(x1)))
9(7(x1)) → 7(5(x1))
7(2(x1)) → 4(x1)
7(0(x1)) → 9(3(x1))
6(9(x1)) → 9(x1)
9(5(9(x1))) → 5(7(x1))
4(x1) → 9(6(6(x1)))
9(x1) → 6(7(x1))
6(2(x1)) → 7(7(x1))
2(4(x1)) → 0(7(x1))
6(6(x1)) → 3(x1)
0(3(x1)) → 5(3(x1))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].


The following pairs can be oriented strictly and are deleted.


21(8(x1)) → 41(x1)
21(8(x1)) → 71(x1)
The remaining pairs can at least be oriented weakly.

21(4(x1)) → 71(x1)
91(5(9(x1))) → 71(x1)
91(x1) → 71(x1)
51(2(6(x1))) → 41(x1)
41(x1) → 91(6(6(x1)))
91(7(x1)) → 51(x1)
41(x1) → 61(x1)
51(2(6(x1))) → 61(2(4(x1)))
91(7(x1)) → 71(5(x1))
71(0(x1)) → 91(3(x1))
61(2(x1)) → 71(7(x1))
51(2(6(x1))) → 21(4(x1))
61(2(x1)) → 71(x1)
71(2(x1)) → 41(x1)
Used ordering: Polynomial interpretation [25,35]:

POL(5(x1)) = 0   
POL(9(x1)) = 0   
POL(4(x1)) = 0   
POL(8(x1)) = 1/4   
POL(51(x1)) = 0   
POL(71(x1)) = 0   
POL(1(x1)) = (9/4)x_1   
POL(21(x1)) = (4)x_1   
POL(41(x1)) = 0   
POL(7(x1)) = 0   
POL(3(x1)) = 0   
POL(2(x1)) = 3 + (4)x_1   
POL(61(x1)) = 0   
POL(6(x1)) = 0   
POL(91(x1)) = 0   
POL(0(x1)) = 0   
The value of delta used in the strict ordering is 1.
The following usable rules [17] were oriented:

4(7(x1)) → 1(3(x1))
2(8(x1)) → 7(x1)
9(7(x1)) → 7(5(x1))
6(2(x1)) → 7(7(x1))
7(0(x1)) → 9(3(x1))
0(3(x1)) → 5(3(x1))
7(2(x1)) → 4(x1)
9(5(9(x1))) → 5(7(x1))
6(9(x1)) → 9(x1)
5(9(x1)) → 0(x1)
5(2(6(x1))) → 6(2(4(x1)))
4(x1) → 9(6(6(x1)))
9(x1) → 6(7(x1))
5(3(x1)) → 6(0(x1))
2(4(x1)) → 0(7(x1))
6(6(x1)) → 3(x1)
2(8(x1)) → 4(x1)
4(x1) → 5(2(3(x1)))



↳ QTRS
  ↳ DependencyPairsProof
    ↳ QDP
      ↳ DependencyGraphProof
        ↳ AND
          ↳ QDP
          ↳ QDP
            ↳ QDPOrderProof
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

21(4(x1)) → 71(x1)
91(5(9(x1))) → 71(x1)
91(x1) → 71(x1)
51(2(6(x1))) → 41(x1)
41(x1) → 91(6(6(x1)))
91(7(x1)) → 51(x1)
41(x1) → 61(x1)
51(2(6(x1))) → 61(2(4(x1)))
91(7(x1)) → 71(5(x1))
71(0(x1)) → 91(3(x1))
61(2(x1)) → 71(7(x1))
51(2(6(x1))) → 21(4(x1))
61(2(x1)) → 71(x1)
71(2(x1)) → 41(x1)

The TRS R consists of the following rules:

2(7(x1)) → 1(8(x1))
2(8(1(x1))) → 8(x1)
2(8(x1)) → 4(x1)
5(9(x1)) → 0(x1)
4(x1) → 5(2(3(x1)))
5(3(x1)) → 6(0(x1))
2(8(x1)) → 7(x1)
4(7(x1)) → 1(3(x1))
5(2(6(x1))) → 6(2(4(x1)))
9(7(x1)) → 7(5(x1))
7(2(x1)) → 4(x1)
7(0(x1)) → 9(3(x1))
6(9(x1)) → 9(x1)
9(5(9(x1))) → 5(7(x1))
4(x1) → 9(6(6(x1)))
9(x1) → 6(7(x1))
6(2(x1)) → 7(7(x1))
2(4(x1)) → 0(7(x1))
6(6(x1)) → 3(x1)
0(3(x1)) → 5(3(x1))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.